FDL - Step of Proof: complete_nat_ind_with_y

Step of Proof: complete_nat_ind_with_y

Inference at * 1 1 2
Iof proof for Lemma complete nat ind with y:

1. P :

{k}
2. g :

i:

. (

j:

i. P(j))

P(i)
3. Y(

f,x. g(x,f))

Void

Void

Y(

f,x. g(x,f))

(

i:

. P(i))

by Assert

n:

. Y(

f,x. g(x,f))

(

m:

n. P(m))

1: .....assertion..... NILNIL

1:

n:

. Y(

f,x. g(x,f))

(

m:

n. P(m))

2:

2: 4.

n:

. Y(

f,x. g(x,f))

(

m:

n. P(m))

2:

Y(

f,x. g(x,f))

(

i:

. P(i))

.

Definitions , t T, x:A. B(x), {i..j}, #$n, x(s), Y, x.A(x), f(a)